\begin{tabbing}
$\forall$${\it es}$:ES, $A$, $B$, $P$, $Q$:(E$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$e$:E. $\neg$($A$($e$) \& $B$($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. $\neg$($P$($e$) \& $Q$($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. Dec($P$($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. Dec($A$($e$)))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. Dec($B$($e$)))
\\[0ex]$\Rightarrow$ \=($\forall$$f$:(\{$e$:E$\mid$ $A$($e$)\} $\rightarrow$\{$e$:E$\mid$ $P$($e$)\} ), $g$:(\{$e$:E$\mid$ $B$($e$)\} $\rightarrow$\{$e$:E$\mid$ $Q$($e$)\} ).\+
\\[0ex]$P$ $\leftarrow\leftarrow$ $f$$--$ $A$
\\[0ex]$\Rightarrow$ $Q$ $\leftarrow\leftarrow$ $g$$--$ $B$
\\[0ex]$\Rightarrow$ ($\exists$\=$h$:\{$e$:E$\mid$ ($A$($e$)) $\vee$ ($B$($e$))\} $\rightarrow$\{$e$:E$\mid$ ($P$($e$)) $\vee$ ($Q$($e$))\} \+
\\[0ex]($\lambda$$e$.($P$($e$)) $\vee$ ($Q$($e$)) $\leftarrow\leftarrow$ $h$$--$ $\lambda$$e$.($A$($e$)) $\vee$ ($B$($e$))
\\[0ex]\& ($\forall$$e$:\{$e$:E$\mid$ ($A$($e$)) $\vee$ ($B$($e$))\} . ($A$($e$)) $\Rightarrow$ ($h$($e$) = $f$($e$)))
\\[0ex]\& ($\forall$$e$:\{$e$:E$\mid$ ($A$($e$)) $\vee$ ($B$($e$))\} . ($\neg$($A$($e$))) $\Rightarrow$ ($h$($e$) = $g$($e$))))))
\-\-
\end{tabbing}